#|;;;; Created on 2010-12-20 00:08:48
(defun unify (x y &optional subst)
  "Tries unifies two expressions x and y returning the substitution list that unifies them"
  (cond ((equal x y) subst)
        ((equal subst 'fail) 'fail)
        ((var? x) (unify-variable x y subst))
        ((var? y) (unify-variable y x subst))
        ((or (atom x) (atom y)) 'fail)
        (t (unify (rest x) (rest y) (unify (first x) (first y) subst)))
   )
 )

(defun unify-variable (var val subst)
"Unify var with val, using (and possibly extending) subst."
	(cond ((equal var val) subst)
		  ((bound? var subst)(unify (lookup var subst) val subst))
			;; New condition: dereference val when it is a variable
		  ((and (var? val) (bound? val subst))(unify var (lookup val subst) subst))
		  ((occurs-in? var val subst) 'fail)
		  (t (extend-subst var  val subst))
    )
 )
(defun occurs-in? (var x subst)
"Does var occur anywhere inside x?"
  (cond ((equal var x) t)
    ((bound? x subst) (occurs-in? var (lookup x subst) subst))
    ((consp x) (or (occurs-in? var (first x) subst)(occurs-in? var (rest x) subst)))
    (t nil)
    )
  )
(defun var? (x) "Is x a variable?" (member x '(U V X Y Z)))
(defun bound? (x subst) "Is x a bound variable?" (assoc x subst))
(defun lookup (var subst) (cdr (cdr (assoc var subst))))
(defun replace-any-where-rec1 (var val cons-list)
(if (consp (cdr cons-list))
  (if (member var (cdr cons-list))
    (rplaca (member var cons-list) val)
    (if (rest cons-list)
		(replace-any-where-rec1 var val (rest cons-list))
    )
  )
  (if (equal var (cdr cons-list))
	(setf (cdr cons-list) val)
  )
  )
 )
(defun replace-any-where-rec2 (var val cons-list)
	(if (consp val)
		(if (member (car cons-list) val)
			(rplaca (member (car cons-list) val)(cdr (cdr cons-list)))
			(replace-any-where-rec2 var (rest val) cons-list)
		)
		(if (equal val(car cons-list))
			(setf val (cdr (cdr cons-list)))
		)
	)
 )
(defun replace-any-where (var val subst)
  (dotimes (i (length subst))
    (replace-any-where-rec1 var val (nth i subst))
	(replace-any-where-rec2 var val (nth i subst))
    )
  )
(defun extend-subst (var val subst) 
  (replace-any-where var val subst)
  (if (consp val)
  (cons (cons var (cons '/ val )) subst)
  (cons (cons var (cons '/ (cons val ()))) subst)
  )
 )
(defun apply-subst (term subst)
  (if (consp term)
      (dotimes (i (length term))
        (setf (nth i term) (apply-subst (nth i term) subst))
        )
      (let ((val (car (lookup term subst))))
        (if val
            (setf term val)
            )
        term
        )
      )
  term
  )
(defun apply-subst-helper (term subst)
  (if (consp term)
      (dotimes (i (length term))
        (setf (nth i term) (apply-subst-helper (nth i term) subst))
        )
      (let ((val (lookup term subst)))
        (if val
            (setf term val)
            )
        term
        )
      )
  )
|#